Nuprl Lemma : assert_dec2bool 4,23
d:Decision. dec2bool(d)  d 
latex

DefinitionsDecision, dec2bool(d), b, true, false, x:A. B(x), Top, True, P  Q, P & Q, P  Q, P  Q, t  T, False
Lemmasfalse wf, true wf, top wf

origin